Nuprl Lemma : haslink_wf 0,22
M:(IdLnkIdType), l:IdLnk, m:Msg(M). haslink(l;m)  Prop 
latex

Definitionshaslink(l;m), Prop, mlnk(m), Msg(M), x:A. B(x), IdLnk, Id, t  T
LemmasId wf, IdLnk wf, Msg wf, mlnk wf

origin